Skip to content

Loop abstraction [depends-on: #2707] #2871

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wants to merge 2 commits into from
Closed

Loop abstraction [depends-on: #2707] #2871

wants to merge 2 commits into from

Conversation

zhixing-xu
Copy link
Contributor

@zhixing-xu zhixing-xu commented Aug 30, 2018 •
edited
Loading

Two flags '--abstract-loops', '--abstractset' are added into goto-instrument and cbmc to support automated loop abstraction for given program.

The goal of this loop abstraction method is to prove memory safety in specific loops without having to unwind them.

If memory safety assertions in a loop are only decided by the loop variables and values unchanged in the loop, and the assertions outside the loop does not depend on loop contents; the loop could be reduced into 1 iteration (shrinkable), by making the loop variables nondet with constraints inflicted by the loop condition. As illustrated in the following example:

Original code:

for(int i=0; i<N; i++){
    for(int j=0; j<M; j++){
        ...
        image[f(i,j)] = value; 
        assert(f(i,j) in bound);
    }
}

After abstraction

i=nondet_int();
j=nondet_int();
assume i<=N && i>=0;
assume j<=M && j>=0;
image[f(i,j)] = value; 
assert(f(i,j) in bound);

'--abstract-loops' enables the method and '--abstractset' allows user to specify loops to be reduced. The method first check if the loops follow the property that allows them to be abstracted by analyzing the data dependence of the loop variables and assertions. For the loops following the property, it proceeds to do the abstraction on them.

This PR also includes #2707, which gives more accurate data dependency through function calls, thus helping decide the loop shrinkability problem better.
It would beneficial to also include #2646, #2694, they give more accurate data dependency for dynamic objects. The regression test abstract-loops3 would pass with these patches.

@zhixing-xu zhixing-xu changed the title Loop abstract Loop abstraction Aug 31, 2018
@peterschrammel
Copy link
Member

Thanks, @zhixing-xu for your contribution. While we are going to review this in more detail, could you please the compilation, linting and formatting errors?

  • Compilation errors on Windows:
cl -DSATCHECK_MINISAT2  -DHAVE_MINISAT2 /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF -I .. /nologo /c /EHsc abstract_loops.cpp /Foabstract_loops.obj
abstract_loops.cpp
abstract_loops.cpp(363): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(363): error C3861: 'inserter': identifier not found
abstract_loops.cpp(372): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(372): error C3861: 'inserter': identifier not found
abstract_loops.cpp(402): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data
abstract_loops.cpp(531): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(531): error C3861: 'inserter': identifier not found
make[2]: *** [../common:222: abstract_loops.obj] Error 2

@tautschnig tautschnig changed the title Loop abstraction Loop abstraction [depends-on: #2707] Feb 25, 2019
@tautschnig tautschnig self-assigned this Feb 25, 2019
@tautschnig tautschnig force-pushed the loop_abstract branch 4 times, most recently from 26e58d7 to 35eba37 Compare February 25, 2019 17:55
@zhixing-xu @tautschnig
Refine data dependency across function calls
f0e7305 
When generating dependences for a parameter in a function call, its data
dependence node is set to be the line this function call happens. The result is
unrelated variables are pulled into the dependence chain.

The fix does a 1-1 mapping between the symbols of function call parameters and
the symbols of the arguments given for the call.
@zhixing-xu @tautschnig
Loop shrinking
ea8504e 
Enables proving properties in selected loops without having to unwind them.
Based on "Property Checking Array Programs Using Loop Shrinking" by Shrawan
Kumar, Amitabha Sanyal, Venkatesh R and Punit Shah, TACAS 2018.
@TGWDB
Copy link
Contributor

TGWDB commented May 3, 2023

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

@TGWDB TGWDB closed this May 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@smowton smowton Awaiting requested review from smowton

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

@thk123 thk123 Awaiting requested review from thk123

@danpoe danpoe Awaiting requested review from danpoe

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@owen-mc-diffblue owen-mc-diffblue Awaiting requested review from owen-mc-diffblue

Assignees

@tautschnig tautschnig

@zhixing-xu zhixing-xu

Labels
dependent - do not merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@zhixing-xu @peterschrammel @TGWDB @tautschnig